T:Type, a,b:T, l1,l2:(T List).
iseg(T; cons(a; l1); cons(b; l2))  ((a = b)  iseg(T; l1; l2)) 

latex

Definitions	prop{i:l}, t  T, P  Q, P  Q, x:A. B(x), P  Q, iseg(T; l1; l2), P  Q, x:A. B(x), ||as||, ge(i; j), Y, listp(A), append(as; bs), tl(l), hd(l)
Lemmas	append wf, tl wf, hd wf, ge wf, non neg length, length wf1, lt int wf, assert wf, assert of lt int, listp wf